Luật tiên đề rỗng

{ P }   skip   { P } {\displaystyle {\frac {}{\{P\}\ {\textbf {skip}}\ \{P\}}}\!}

Luật về phát biểu gán

Tiên đề gán chỉ ra rằng sau phép gán, bất kỳ vị từ nào chứa biến là true đối với vế phải phép gán:

{ P [ E / x ] }   x = E   { P } {\displaystyle {\frac {}{\{P[E/x]\}\ x=E\ \{P\}}}\!}

Ở đây P [ E / x ] {\displaystyle P[E/x]} chỉ ra rằng biểu thức P trong đó tất cả các lần xuất hiện tự do của biến x đã được thay bằng biểu thức E.

Ý nghĩa của tiên đề gán này là giá trị đúng sai của { P [ E / x ] } {\displaystyle \{P[E/x]\}} là tương đương với giá trị đúng sai của { P } {\displaystyle \{P\}} sau khi gán. Do đó nếu { P [ E / x ] } {\displaystyle \{P[E/x]\}} là true trước phép gán, nhờ tiên đề gán { P } {\displaystyle \{P\}} cũng sẽ true sau phép gán. Ngược lại, nếu { P [ E / x ] } {\displaystyle \{P[E/x]\}} là false trước phép gán, thì chắc chắn { P } {\displaystyle \{P\}} phải là false sau phép gán.

Các ví dụ về những bộ ba đúng:

• { x + 1 = 43 }   y := x + 1   { y = 43 } {\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}\!}
• { x + 1 ≤ N }   x := x + 1   { x ≤ N }   {\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\}\ \!}

Tiên đề gán do Hoare đưa ra không áp dụng vào trường hợp có nhiều hơn một tên cùng chỉ một giá trị lưu trữ. Ví dụ,

{ y = 3 }   x := 2   { y = 3 } {\displaystyle \{y=3\}\ x:=2\ \{y=3\}}

là không đúng nếu x và y cùng đại diện cho một biến, vì không có tiền điều kiện nào có thể khiến cho y bằng 3 sau khi x được gán bằng 2.

Luật ghép

Luật về phát biểu ghép của Hoare áp dụng cho những chương trình được thực thi tuần tự S và T, trong đó S thực thi trước T và được viết là S;T.

{ P }   S   { Q }   { Q }   T   { R } { P }   S ; T   { R } {\displaystyle {\frac {\{P\}\ S\ \{Q\}\,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!}

Ví dụ, xét hai phát biểu sau:

{ x + 1 = 43 }   y := x + 1   { y = 43 } {\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}}

và

{ y = 43 }   z := y   { z = 43 } {\displaystyle \{y=43\}\ z:=y\ \{z=43\}}

Theo luật ghép, ta có thể kết luận:

{ x + 1 = 43 }   y := x + 1 ; z := y   { z = 43 } {\displaystyle \{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}}

Luật điều kiện

{ B ∧ P }   S   { Q }   { ¬ B ∧ P }   T   { Q } { P }   if   B   then   S   else   T   endif   { Q } {\displaystyle {\frac {\{B\wedge P\}\ S\ \{Q\}\,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}\!}

Luật While

{ P ∧ B }   S   { P } { P }   while   B   do   S   done   { ¬ B ∧ P } {\displaystyle {\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!}

Ở đây P là điều kiện bất biến của vòng lặp.

Luật hệ quả

P ′ →   P   { P }   S   { Q }   Q →   Q ′ { P ′   }   S   { Q ′ } {\displaystyle {\frac {P^{\prime }\rightarrow \ P\,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \,\ Q\rightarrow \ Q^{\prime }}{\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}\!}

Luật While dành cho tính đúng đắn toàn phần

{ P ∧ B ∧ t = z }   S   { P ∧ t < z }   P → t ≥ 0 { P }   while   B   do   S   done   { ¬ B ∧ P } {\displaystyle {\frac {\{P\wedge B\wedge t=z\}\ S\ \{P\wedge t<z\}\,\ P\rightarrow t\geq 0}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!}

Trong luật này, ngoài việc giữ các điều kiện bất biến vòng lặp, ta cũng phải chứng minh dừng bằng cách chứng minh giá trị của một số hạng giảm dần sau mỗi lần lặp, ở đây là t. Chú ý rằng t phải là giá trị thuộc tập chắc chắn, để cho mỗi bước lặp có thể tính được bằng cách giảm giá trị đi một chuỗi hữu hạn.